\begin{tabbing}
$\forall$\=${\it es}$:ES, ${\it Cmd}$, ${\it Rsp}$:Type, ${\it isupdate}$:(${\it Cmd}$$\rightarrow\mathbb{B}$), ${\it In}$:AbsInterface(${\it Cmd}$), ${\it Out}$:AbsInterface(${\it Rsp}$),\+
\\[0ex]${\it Delta}$:((\{$c$:${\it Cmd}$$\mid$ $\uparrow$(${\it isupdate}$($c$))\}  List)$\rightarrow$${\it Rsp}$),
\\[0ex]$Q$:((\{$c$:${\it Cmd}$$\mid$ $\uparrow$(${\it isupdate}$($c$))\}  List)$\rightarrow$\{$c$:${\it Cmd}$$\mid$ $\neg$($\uparrow$(${\it isupdate}$($c$)))\} $\rightarrow$${\it Rsp}$).
\-\\[0ex]approx\_sm(${\it es}$; ${\it In}$; ${\it Out}$; ${\it Cmd}$; ${\it isupdate}$; ${\it Rsp}$; ${\it Delta}$; $Q$) $\in$ $\mathbb{P}$
\end{tabbing}